\begin{tabbing}
$\forall$${\it es}$:event\_system\{i:l\}, $x$,$i$:Id, $T$:Type.
\\[0ex]($\forall$$x$,$y$:$T$. decidable(($x$ = $y$ $\in$ $T$)))
\\[0ex]$\Rightarrow$ es{-}dtype(${\it es}$; $i$; $x$; $T$)
\\[0ex]$\Rightarrow$ \=($\forall$${\it e'}$,$e$:es{-}E(${\it es}$).\+
\\[0ex]es{-}le(${\it es}$; $e$; ${\it e'}$)
\\[0ex]$\Rightarrow$ (loc(${\it e'}$) = $i$)
\\[0ex]$\Rightarrow$ ($\neg$(es{-}after(${\it es}$; $x$; ${\it e'}$) = es{-}when(${\it es}$; $x$; $e$) $\in$ $T$))
\\[0ex]$\Rightarrow$ ($\exists$\=${\it ev}$:es{-}E(${\it es}$)\+
\\[0ex]((es{-}le(${\it es}$; $e$; ${\it ev}$) $\wedge$ es{-}le(${\it es}$; ${\it ev}$; ${\it e'}$))
\\[0ex]$\wedge$ ($\neg$(es{-}after(${\it es}$; $x$; ${\it ev}$) = es{-}when(${\it es}$; $x$; ${\it ev}$) $\in$ $T$)))))
\-\-
\end{tabbing}